/*
 * Rule.h
 *
 *  Created on: Apr 30, 2012
 *      Author: kobe
 */

#ifndef RULE_H_
#define RULE_H_

#include "Sequent.h"
#include <string>
#include "Proposition.h"
#include "Context.h"

enum RuleType {
	PRAPP = 0,
	APP = 1,
	NAVAPP = 2,
	OTHER = 3,
	KERNEL = 4
};

class Rule {
public:
	Rule();
	virtual ~Rule();
	virtual std::vector<Sequent*> run(Sequent*);
	virtual std::string toString();
	virtual std::string toLatex();
	virtual bool isVariousRule();
	virtual bool isLoopRule();
	virtual void popLastSequent();
	virtual RuleType getRuleType();
protected:
	Context* searchOperatorInContext(Context*, ModalLogic);
	Context* searchActionOperatorInContext(Context*, ModalLogic);
	Context* searchContextInContext(Context*, Context*);
};

std::vector<Rule*> registerAllRules();
std::vector<Rule*> registerAllRulesEpistemic();

#endif /* RULE_H_ */
